i:Id, L:Knd List, l:IdLnk, tg:Id.
@i: only L sends on (l with tg)  Dsys
& (D:Dsys.
& (@i: only L sends on (l with tg)  D
& ( D realizes es. e:E. loc(e) = i  Id  null(sends(l,tg,e))  (kind(e)  L)) 

latex

Definitions	only L sends on (l with tg), @i: only L sends on (l with tg), IdLnk, @i: A, if b t else f fi, a = b, MsgA, , A & B, Dsys, x. t(x), {T}, E, Id, loc(e), P  Q, Prop, A, b, null(as), (Msg on l), sends(l,tg,e), (x  l), Knd, kind(e), ES, es is an event system of D, x:A. B(x), t  T
Lemmas	d-es wf, event system wf, es-kind wf, l member wf, es-tg-sends wf, es-Msgl wf, null wf, assert wf, not wf, es-loc wf, es-E wf, realizes-monotone-wrt-sub, dsys wf, ma-empty wf, ma-single-sframe wf, msga wf, eq id wf, ifthenelse wf, Id wf, Knd wf, IdLnk wf, sframe-rule